| 1: | a__nats | → a__adx(a__zeros) | |
| 2: | a__zeros | → cons(0,zeros) | |
| 3: | a__incr(cons(X,Y)) | → cons(s(X),incr(Y)) | |
| 4: | a__adx(cons(X,Y)) | → a__incr(cons(X,adx(Y))) | |
| 5: | a__hd(cons(X,Y)) | → mark(X) | |
| 6: | a__tl(cons(X,Y)) | → mark(Y) | |
| 7: | mark(nats) | → a__nats | |
| 8: | mark(adx(X)) | → a__adx(mark(X)) | |
| 9: | mark(zeros) | → a__zeros | |
| 10: | mark(incr(X)) | → a__incr(mark(X)) | |
| 11: | mark(hd(X)) | → a__hd(mark(X)) | |
| 12: | mark(tl(X)) | → a__tl(mark(X)) | |
| 13: | mark(cons(X1,X2)) | → cons(X1,X2) | |
| 14: | mark(0) | → 0 | |
| 15: | mark(s(X)) | → s(X) | |
| 16: | a__nats | → nats | |
| 17: | a__adx(X) | → adx(X) | |
| 18: | a__zeros | → zeros | |
| 19: | a__incr(X) | → incr(X) | |
| 20: | a__hd(X) | → hd(X) | |
| 21: | a__tl(X) | → tl(X) | |
| 22: | A__NATS | → A__ADX(a__zeros) | |
| 23: | A__NATS | → A__ZEROS | |
| 24: | A__ADX(cons(X,Y)) | → A__INCR(cons(X,adx(Y))) | |
| 25: | A__HD(cons(X,Y)) | → MARK(X) | |
| 26: | A__TL(cons(X,Y)) | → MARK(Y) | |
| 27: | MARK(nats) | → A__NATS | |
| 28: | MARK(adx(X)) | → A__ADX(mark(X)) | |
| 29: | MARK(adx(X)) | → MARK(X) | |
| 30: | MARK(zeros) | → A__ZEROS | |
| 31: | MARK(incr(X)) | → A__INCR(mark(X)) | |
| 32: | MARK(incr(X)) | → MARK(X) | |
| 33: | MARK(hd(X)) | → A__HD(mark(X)) | |
| 34: | MARK(hd(X)) | → MARK(X) | |
| 35: | MARK(tl(X)) | → A__TL(mark(X)) | |
| 36: | MARK(tl(X)) | → MARK(X) | |